\subsection{Skolem functions}
\begin{definition}
    Let \( \mathcal T \) be an \( \mathcal L \)-theory, and let \( \varphi(\vb x, y) \) be an \( \mathcal L \)-formula where \( \vb x \) is nonempty.
    A \emph{Skolem function} for \( \varphi \) is an \( \mathcal L \)-term \( t \) such that
    \[ \mathcal T \vdash \forall \vb x.\, (\exists y.\, \varphi(\vb x, y) \to \varphi(\vb x, t(\vb x))) \]
    A \emph{skolemisation} of an \( \mathcal L \)-theory \( \mathcal T \) is a language \( \mathcal L^+ \supseteq \mathcal L \) and an \( \mathcal L^+ \)-theory \( \mathcal T^+ \supseteq \mathcal T \) such that
    \begin{enumerate}
        \item every \( \mathcal L \)-structure that models \( \mathcal T \) can be expanded to an \( \mathcal L^+ \)-structure that models \( \mathcal T^+ \);
        \item \( \mathcal T^+ \) has Skolem functions for any \( \mathcal L^+ \)-formula \( \varphi(\vb x, y) \) where \( \vb x \) is nonempty.
    \end{enumerate}
    A theory is called a \emph{Skolem theory} if it is a skolemisation of itself.
\end{definition}
By `expanded', we mean that \( \mathcal T \) is given interpretations to the elements of \( \mathcal L^+ \setminus \mathcal L \), but no new objects are added.
\begin{proposition}
    Let \( \mathcal T \) be an \( \mathcal L \)-theory, and let \( \mathcal F \) be a collection of \( \mathcal L \)-formulae including all atomic formulae and closed under Boolean operations.
    Suppose that for every formula \( \psi(\vb x, y) \in \mathcal F \), there exists \( \varphi(\vb x) \in \mathcal F \) with
    \[ \mathcal T \vdash \forall \vb x.\, (\exists y.\, \psi(\vb x, y) \Leftrightarrow \varphi(\vb x)) \]
    Then, every \( \mathcal L \)-formula is equivalent to one in \( \mathcal F \) with the same free variables modulo \( \mathcal T \) (that is, \( \mathcal T \) proves they are equivalent).
\end{proposition}
\begin{proof}
    We proceed by induction on the length of formulae.
    The case of existential formulae is the only nontrivial inductive step.
    Consider the formula \( \exists y,\, \psi(\vb x, y) \).
    By the inductive hypothesis, \( \psi(\vb x, y) \) is \( \mathcal T \)-equivalent to \( \psi'(\vb x, y) \in \mathcal F \).
    Then, there is some \( \varphi(\vb x) \in \mathcal F \) such that
    \[ \mathcal T \vdash \forall \vb x.\, (\exists y.\, \psi'(\vb x, y) \Leftrightarrow \varphi(\vb x)) \]
    Thus the formula \( \exists y,\, \psi(\vb x, y) \) in question is \( \mathcal T \)-equivalent to \( \varphi(\vb x) \in \mathcal F \).
\end{proof}
\begin{proposition}
    Let \( \mathcal T \) be a Skolem theory.
    Then,
    \begin{enumerate}
        \item every \( \mathcal L \)-formula \( \varphi(\vb x) \) where \( \vb x \) is nonempty is equivalent modulo \( \mathcal T \) to some quantifier-free \( \varphi^\star(\vb x) \);
        \item if \( \mathcal N \vDash \mathcal T \) and \( X \subseteq \mathcal N \), then either \( \langle X \rangle_{\mathcal N} = \varnothing \) or \( \langle X \rangle_{\mathcal N} \preceq \mathcal N \).
    \end{enumerate}
\end{proposition}
\begin{remark}
    When \( \mathcal N \) is a model of a Skolem theory, \( \langle X \rangle_{\mathcal N} \) is sometimes called the \emph{Skolem hull} of \( X \).
\end{remark}
\begin{proof}
    \emph{Part (i).}
    Clearly, \( \varphi(\vb x, t(\vb x)) \to \exists y.\, \varphi(\vb x, y) \) in any model.
    So having Skolem functions means that
    \[ \mathcal T \vdash \forall \vb x.\, (\exists y.\, \varphi(\vb x, y) \Leftrightarrow \varphi(\vb x, t(\vb x))) \]
    completing the proof by the previous proposition.

    \emph{Part (ii).}
    We proceed by the Tarski--Vaught test.
    Let \( \mathcal M = \langle X \rangle_{\mathcal N}, \vb m \in \mathcal M \), and let \( \varphi(\vb x, y) \) be such that
    \[ \mathcal N \vDash \exists y.\, \varphi(\vb m, y) \]
    Then as \( \mathcal N \) has Skolem functions, there exists an \( \mathcal L \)-term \( t \) such that
    \[ \mathcal N \vDash \varphi(\vb m, t(\vb m)) \]
    But \( \mathcal M \) is closed under the interpretation of function symbols as it is a substructure, so \( t(\vb m) \in \mathcal M \).
    Thus
    \[ \mathcal M \vDash \exists y.\, \varphi(\vb m, y) \]
    as required.
\end{proof}

\subsection{Skolemisation theorem}
\begin{theorem}
    Every first-order language \( \mathcal L \) can be expanded to some \( \mathcal L^+ \supseteq \mathcal L \) that includes an \( \mathcal L^+ \)-theory \( \Sigma \) such that
    \begin{enumerate}
        \item \( \Sigma \) is a Skolem \( \mathcal L^+ \)-theory;
        \item any \( \mathcal L \)-structure can be expanded to an \( \mathcal L^+ \)-structure that models \( \Sigma \); and
        \item \( \abs{\mathcal L^+} = \abs{\mathcal L} \).
    \end{enumerate}
\end{theorem}
\begin{proof}
    We will design \( \mathcal L^+ \) to include Skolem functions for each suitable formula.
    If \( \chi(\vb x, y) \) is an \( \mathcal L \)-formula with \( \vb x \) nonempty, we add a function symbol \( F_\chi \) of arity \( \abs{\vb x} \).
    Performing this for all \( \mathcal L \)-formulae of this form, we obtain a language \( \mathcal L' \supseteq \mathcal L \).
    Next, define \( \Sigma(\mathcal L) \) to be the set of \( \mathcal L \)-sentences that enforce the correct behaviour of the \( F_\chi \):
    \[ \forall \vb x.\, (\exists y.\, \chi(\vb x, y) \to \chi(\vb x, F_\chi(\vb x))) \]
    Note that \( \Sigma(\mathcal L) \) is an \( \mathcal L' \)-theory, not an \( \mathcal L \)-theory; there may be existentials in \( \mathcal L' \) without explicit witnesses.
    We can overcome this issue by iterating this construction \( \omega \) times and taking the union.
    Formally, we recursively define
    \[ \mathcal L_0 = \mathcal L;\quad \mathcal L_{n+1} = \mathcal L_n';\quad \Sigma_0 = \varnothing; \quad \Sigma_{n+1} = \Sigma_n \cup \Sigma(\mathcal L_n) \]
    Then we can set
    \[ \mathcal L^+ = \bigcup_{n < \omega} \mathcal L_n;\quad \Sigma = \bigcup_{n < \omega} \Sigma_n \]
    First, note that \( \Sigma \) is a Skolem theory.
    This is because each \( \mathcal L^+ \)-formula is in \( \mathcal L_n \) for some \( n < \omega \), so \( \Sigma_{n+1} \subseteq \Sigma \) asserts that it has a Skolem function.
    It is also clear to see that \( \abs{\mathcal L^+} = \abs{\mathcal L} \) using basic cardinal arithmetic.

    To prove property (ii), it suffices to show that each \( \mathcal L \)-theory can be expanded into an \( \mathcal L' \)-theory that models \( \Sigma(\mathcal L) \); we can then proceed by induction.
    Note that this argument will use the axiom of choice.
    Let \( \mathcal M \) be an \( \mathcal L \)-structure.
    We can assume \( \mathcal M \neq \varnothing \); if \( \mathcal M = \varnothing \) then all sentences in \( \Sigma \) would be vacuously true and there would be nothing to prove.
    We now expand \( \mathcal M \) into an \( \mathcal L' \)-structure \( \mathcal M \) in the following way.
    Consider \( \chi(\vb x, y) \) where \( \vb x \) is nonempty and \( \vb m \in \mathcal M \).
    If
    \[ \mathcal M \vDash \exists b.\, \chi(\vb m, b) \]
    then we can choose such a \( b \) and interpret \( F_\chi(\vb m) \) as this value.
    If
    \[ \mathcal M \nvDash \exists b.\, \chi(\vb m, b) \]
    then we interpret \( F_\chi(\vb m) \) as an arbitrary model element, say, \( \vb m_0 \).
    By construction, \( \mathcal M' \) models \( \Sigma(\mathcal L) \).
\end{proof}
\begin{corollary}
    Any \( \mathcal L \)-theory \( \mathcal T \) admits a skolemisation \( \mathcal T^+ \) in a language \( \mathcal L^+ \) of the same size as \( \mathcal L \).
\end{corollary}
\begin{proof}
    Take \( \mathcal T^+ = \mathcal T \cup \Sigma \).
    Any model of \( \mathcal T^+ \) models \( \Sigma \), so \( \mathcal T^+ \) has Skolem functions.
    Moreover, any \( \mathcal L \)-structure that models \( \mathcal T \) can be extended to one that models \( \Sigma \), which will therefore model \( \mathcal T^+ \).
\end{proof}
\begin{corollary}[downward L\"owenheim--Skolem theorem]
    Let \( \mathcal M \) be an \( \mathcal L \)-structure, and let \( X \subseteq \mathcal M \).
    Let \( \kappa \) be a cardinal such that
    \[ \abs{\mathcal L} + \abs{X} \leq \kappa \leq \abs{\mathcal M} \]
    Then \( \mathcal M \) has an elementary substructure of size \( \kappa \) that contains \( X \).
\end{corollary}
\begin{proof}
    Let \( X \subseteq Y \subseteq \mathcal M \) and \( \abs{Y} = \kappa \).
    Let \( \mathcal M' \) be an expansion of \( \mathcal M \) to a Skolem theory, and consider the Skolem hull \( \langle Y \rangle_{\mathcal M'} \).
    \( \langle Y \rangle_{\mathcal M'} \) must be an elementary substructure of \( \mathcal M' \) as \( Y \neq \varnothing \).
    Let \( \mathcal N \) be the \( \mathcal L \)-reduct of \( \langle Y \rangle_{\mathcal M'} \).
    Then \( \mathcal N \) is an elementary substructure of \( \mathcal N \), and \( X \subseteq \mathcal N \).
    It remains to check \( \abs{\mathcal N} = \kappa \).
    \[ \abs{\mathcal N} \leq \abs{Y} + \abs{\mathcal L^+} = \kappa + \abs{\mathcal L} = \kappa = \abs{Y} \leq \abs{\mathcal N} \]
    So \( \abs{\mathcal N} = \kappa \).
\end{proof}

\subsection{Elimination sets}
\begin{definition}
    Let \( \mathcal T \) be an \( \mathcal L \)-theory.
    A set \( F \) of \( \mathcal L \)-formulae is an \emph{elimination set} for \( \mathcal T \) if, for every \( \mathcal L \)-formula \( \varphi \), there is a Boolean combination \( \varphi^\star \) of formulae in \( F \) such that
    \[ \mathcal T \vdash \varphi \Leftrightarrow \varphi^\star \]
    A theory \( \mathcal T \) has \emph{quantifier elimination} if the family of quantifier-free formulae forms an elimination set for \( \mathcal T \).
\end{definition}
Note that a theory having quantifier elimination depends on its underlying language.
Every Skolem theory has quantifier elimination.
\begin{example}
    \begin{enumerate}
        \item Let \( p \in \mathbb C[x] \) be the polynomial \( x^3 - 31x^2 + 6 \) over \( \mathbb C \).
        The sentence \( \exists x.\, p(x) = 0 \) contains a quantifier.
        But as \( \mathbb C \) is algebraically closed, it is equivalent to the quantifier-free sentence \( 1 \neq 0 \vee (-31) \neq 0 \).
        \item A real-valued matrix is invertible if there exists a two-sided inverse.
        This has a quantifier, but there is a quantifier-free sentence equivalent to it, namely, `its determinant is nonzero'.
    \end{enumerate}
\end{example}
\begin{remark}
    \begin{enumerate}
        \item We can check if two models of \( \mathcal T \) are elementarily equivalent by considering just those formulae in an elimination set.
        In particular, to check if a theory is complete, it suffices to check that all sentences in an elimination set are either deducible from the theory or inconsistent with it.
        \item Suppose \( \mathcal L \) is a recursive language, and the map \( \varphi \mapsto \varphi^\star \) is computable.
        Then an algorithm to decide whether \( \mathcal T \) proves any sentence can be produced from one that operates only on the elimination set.
        \item The elementary embeddings \( \mathcal M \rightarrowtail \mathcal N \) are precisely those embeddings that preserve \( \varphi \) and \( \neg \varphi \) for all \( \varphi \) in \( F \).
        So a theory with quantifier elimination is model-complete. % why? check. also check why we need \neg \varphi
        \item The definable sets of a model are precisely the Boolean combinations of sets definable with only formulae in an elimination set.
    \end{enumerate}
\end{remark}
In the next result, we use the notation \( \neg F \) for the set of negations of formulae in \( F \).
\begin{proposition}[syntactic quantifier elimination]
    Let \( \mathcal T \) be an \( \mathcal L \)-theory, and let \( F \) be a family of \( \mathcal L \)-formulae including all atomic formulae.
    Suppose that, for every \( \mathcal L \)-formula of the form
    \[ \theta(\vb x) = \exists y.\, \bigwedge_{i < n} \varphi_i(\vb x, y);\quad \varphi_i \in F \cup \neg F \]
    there exists a Boolean combination \( \theta^\star(\vb x) \) of formulae in \( F \) such that
    \[ \mathcal T \vdash \forall \vb x.\, (\theta(\vb x) \Leftrightarrow \theta^\star(\vb x)) \]
    Then \( F \) is an elimination set for \( \mathcal T \).
\end{proposition}
The proof is similar to a previous proposition.
\begin{example}
    Consider the theory \( \mathcal T_\infty \) of infinite sets in the language with empty signature.
    The only atomic formulae are equalities, and the only terms in the language are variables.
    Using the above proposition, it suffices to eliminate the existential quantifier in formulae \( \varphi(x_0, \dots, x_{n-1}) \) of the form
    \[ \exists y.\, \qty(\bigwedge_{i \in I} y = x_i) \wedge \qty(\bigwedge_{i \in J} y \neq x_i) \wedge \qty(\bigwedge_{i, j \in K} x_i = x_j) \wedge \qty(\bigwedge_{i, j \in L} x_i \neq x_j) \]
    where \( I, J, K, L \subseteq \qty{0, \dots, n-1} \).
    Without loss of generality we can assume \( I \) is empty, as we can easily remove the quantifier in this situation.
    We may also push the quantifier inside the first conjunct.
    \[ \qty(\exists y.\, \bigwedge_{i \in J} y \neq x_i) \wedge \psi(x_0, \dots, x_{n-1});\quad \psi(x_0, \dots, x_{n-1}) = \qty(\bigwedge_{i, j \in K} x_i = x_j) \wedge \qty(\bigwedge_{i, j \in L} x_i \neq x_j) \]
    But the theory of infinite sets proves \( \exists y.\, \bigwedge_{i \in J} y \neq x_i \), so we can conclude that \( \varphi \) and \( \psi \) are equivalent modulo \( \mathcal T \).
\end{example}

\subsection{Amalgamation}
\begin{definition}
    Let \( \mathcal M \) and \( \mathcal N \) be \( \mathcal L \)-structures.
    We write \( \mathcal M \to_1 \mathcal N \) if every existential sentence modelled by \( \mathcal M \) is also modelled by \( \mathcal N \).
\end{definition}
\begin{theorem}[existential amalgamation]
    Let \( \mathcal M \) and \( \mathcal N \) be \( \mathcal L \)-structures, with \( S \subseteq \mathcal M \).
    Suppose there is a homomorphism \( f : \langle S \rangle_{\mathcal M} \to \mathcal N \) such that \( (\mathcal N, f(S)) \to_1 (\mathcal M, S) \).
    Then there is an elementary extension \( \mathcal K \) of \( \mathcal N \) and an embedding \( g : \mathcal M \rightarrowtail \mathcal K \) making the following diagram commute.
\[\begin{tikzcd}
	& {\mathcal K} \\
	{\mathcal M} && {\mathcal N} \\
	& {\langle S \rangle_{\mathcal M}}
	\arrow[tail, from=3-2, to=2-1]
	\arrow["\preceq", tail, from=2-1, to=1-2]
	\arrow["f"', from=3-2, to=2-3]
	\arrow["g"', tail, from=2-3, to=1-2]
\end{tikzcd}\]
\end{theorem}
\begin{proof}
    Let \( \mathcal M, \mathcal N \) be disjoint without loss of generality.
    Consider the \( \mathcal L_{\mathcal M \sqcup \mathcal N} \)-theory
    \[ \mathcal T = \operatorname{Diag}_{\text{el}} \mathcal M \cup \operatorname{Diag} \mathcal N \cup \bigcup_{s \in S} \qty{s = f(s)} \]
    We show this is consistent by compactness; then, a model \( \mathcal K \) will be an elementary extension of \( \mathcal M \), and \( \mathcal N \) embeds into it in such a way that makes the above diagram commute due to the sentences \( s = f(s) \).
    If \( \mathcal T \) is inconsistent, there is a finite set of formulae in \( \operatorname{Diag} \mathcal N \) that are inconsistent with
    \[ \mathcal T' = \operatorname{Diag}_{\text{el}} \mathcal M \cup \bigcup_{s \in S} \qty{s = f(s)} \]
    Taking the conjunction, we can suppose it is a single formula \( \varphi(\vb n) \), where \( \vb n \in \mathcal N \) is a tuple of pairwise distinct elements.
    \[ \mathcal T' \vdash \neg\varphi(\vb n) \]
    Then, using the sentences \( s = f(s) \) and the fact that \( \langle S \rangle_{\mathcal M} \) is generated by \( S \), the formula \( \varphi(\vb n) \) is equivalent modulo \( \mathcal T' \) to some quantifier-free formula \( \psi(\vb s, \vb n') \) where \( \vb s \in S \) and \( \vb n' \in \mathcal N \setminus \im f \).
    \[ \mathcal T' \vdash \neg\psi(\vb s, \vb n') \]
    Now, note that \( \mathcal T' \) has nothing to say about \( \vb n' \), so in fact
    \[ \mathcal T' \vdash \forall \vb x.\, \neg\psi(\vb s, \vb x) \]
    As \( (\mathcal N, f(S)) \to_1 (\mathcal M, S) \), we can convert the universal quantifier above into the negation of an existential quantifier to conclude
    \[ \mathcal N \vdash \neg\exists \vb x.\, \psi(\vb s, \vb x) \]
    so
    \[ \mathcal N \vdash \neg\exists \vb x.\, \psi(\vb s, \vb x) \]
    But \( \varphi(\vb n) \) is in the diagram of \( \mathcal N \), so \( \mathcal N \vdash \exists \vb x.\, \psi(\vb s, \vb x) \), giving a contradiction.
\end{proof}
We can make the following more general definition.
\begin{definition}
    A class \( \mathbb K \) of \( \mathcal L \)-structures has the \emph{amalgamation property} if, given a diagram of elements of \( \mathbb K \)
    % https://q.uiver.app/#q=WzAsMyxbMSwxLCJcXG1hdGhjYWwgQyJdLFswLDAsIlxcbWF0aGNhbCBCIl0sWzIsMCwiXFxtYXRoY2FsIEEiXSxbMCwxLCIiLDAseyJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJob29rIiwic2lkZSI6InRvcCJ9fX1dLFswLDIsIiIsMix7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV1d
    \[\begin{tikzcd}
        {\mathcal B} && {\mathcal A} \\
        & {\mathcal C}
        \arrow[tail, from=2-2, to=1-1]
        \arrow[tail, from=2-2, to=1-3]
    \end{tikzcd}\]
    there is a structure \( \mathcal D \) in \( \mathbb K \) and embeddings making the following diagram commute.
    % https://q.uiver.app/#q=WzAsNCxbMSwyLCJcXG1hdGhjYWwgQyJdLFswLDEsIlxcbWF0aGNhbCBCIl0sWzIsMSwiXFxtYXRoY2FsIEEiXSxbMSwwLCJcXG1hdGhjYWwgRCJdLFswLDEsIiIsMCx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV0sWzAsMiwiIiwyLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoiaG9vayIsInNpZGUiOiJ0b3AifX19XSxbMiwzLCIiLDIseyJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJob29rIiwic2lkZSI6InRvcCJ9fX1dLFsxLDMsIiIsMCx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV1d
    \[\begin{tikzcd}
        & {\mathcal D} \\
        {\mathcal B} && {\mathcal A} \\
        & {\mathcal C}
        \arrow[tail, from=3-2, to=2-1]
        \arrow[tail, from=3-2, to=2-3]
        \arrow[tail, from=2-3, to=1-2]
        \arrow[tail, from=2-1, to=1-2]
    \end{tikzcd}\]
\end{definition}
\begin{definition}
    Let \( \mathbb K \) be a class of \( \mathcal L \)-structures and \( \mathcal M \in \mathbb K \).
    We say that \( \mathcal M \) is \emph{existentially closed in \( \mathbb K \)} if, for every existential formula \( \psi(\vb x) \) and tuple \( \vb m \in \mathcal M \), the existence of an extension \( \mathcal M \subseteq \mathcal N \in \mathbb K \) with \( \mathcal N \vDash \psi(\vb m) \) forces \( \mathcal M \vDash \psi(\vb m) \).
\end{definition}
Note that being existentially closed in \( \mathbb K \) depends on the choice of \( \mathbb K \).
For example, an existentially closed ordered field need not be an existentially closed field.
\begin{example}
    \begin{enumerate}
        \item Every field that is existentially closed in the class of fields is algebraically closed.
        Let \( A \) be an existentially closed field, and view a nontrivial polynomial \( f(\vb y) \) over \( A \) as a statement \( p(\vb a, y) \) where \( p(\vb x, y) \) is a term in the language of rings, and \( \vb a \) is a tuple.
        For instance, \( y^2 + 2y - 3 \) can be seen as \( p(1, 2, 3, y) \), where \( p(x_0, x_1, x_2, y) = x_0 y^2 + x_1 y + (-x_2) \).
        We can replace \( f \) with an irreducible factor and consider the quotient ring \( \faktor{A[y]}{(f)} \), which is an extension of \( A \) over which \( f \) has a root.
        \[ \faktor{A[y]}{(f)} \vDash \exists y.\, p(\vb a, y) = 0 \]
        Since \( f \) is irreducible, this is an extension of fields.
        Thus, as \( A \) is existentially closed,
        \[ A \vDash \exists y.\, p(\vb a, y) = 0 \]
        so \( f \) has a root in \( A \).
        The converse is true, and is one way that Hilbert's Nullstellensatz can be stated.
        \item The existentially closed linear orders are precisely the dense linear orders without endpoints.
        \item The existentially closed ordered fields are precisely the \emph{real closed fields}, which are the ordered fields elementarily equivalent to the real numbers.
        Equivalently, all nonnegative elements are squares, and all odd-degree elements have a root.
    \end{enumerate}
\end{example}
\begin{theorem}
    Let \( \mathbb K \) be a class of \( \mathcal L \)-structures that is closed under isomorphism.
    Suppose that the class of all of the substructures of the structures in \( \mathbb K \) has the amalgamation property.
    Then, every existential \( \mathcal L \)-formula \( \varphi(\vb x) \) is equivalent to a quantifier-free \( \mathcal L \)-formula in all existentially closed structures in \( \mathbb K \).
    In particular, if \( \mathcal T \) is a theory axiomatising existentially closed structures in \( \mathbb K \), then \( \mathcal T \) has quantifier elimination.
\end{theorem}
\begin{proof}
    Let \( \varphi(\vb x) \) be an existential formula.
    We will call a pair \( (\mathcal M, \vb m) \) a \emph{witnessing pair} if \( \mathcal M \) is existentially closed in \( \mathbb K \) and \( \mathcal M \vDash \varphi(\vb m) \).
    For each such pair, let
    \[ \theta_{(\mathcal M, \vb m)} = \bigwedge \qty{\psi \text{ a literal} \mid \mathcal M \vDash \psi(\vb m)} \]
    where the \emph{literals} are the atomic formulae and their negations.
    Let
    \[ \chi(\vb x) = \bigvee_{(\mathcal M, \vb m)} \theta_{(\mathcal M, \vb m)}(\vb x) \]
    Note that the \( \theta \) and \( \chi \) are not first-order formulae, but any conjunction or disjunction over an infinite set is logically equivalent to a finite conjunction or disjunction over a finite subset; this can be seen by applying the compactness theorem.
    It suffices to show that if \( \mathcal N \) is existentially closed in \( \mathbb K \) then
    \[ (\mathcal N \vDash \varphi(\vb n)) \iff (\mathcal N \vDash \chi(\vb n)) \]
    If \( \vb n \in \mathcal N \) is such that \( \mathcal N \vDash \varphi(\vb n) \), then \( (\mathcal N, \vb n) \) is a witnessing pair, and thus \( \mathcal N \vDash \chi(\vb n) \) by construction.
    For the converse, if \( \mathcal N \vDash \chi(\vb n) \), there is a witnessing pair \( (\mathcal M, \vb m) \) such that \( \mathcal N \vDash \theta_{(\mathcal M, \vb m)}(\vb n) \).
    Hence, for each literal \( \psi(\vb x) \),
    \[ (\mathcal M \vDash \psi(\vb m)) \implies (\mathcal N \vDash \psi(\vb n)) \]
    There is thus an embedding \( e : \langle \vb m \rangle_{\mathcal M} \rightarrowtail \mathcal N \) mapping \( \vb m \) to \( \vb n \).
    Applying the amalgamation property, we obtain
    % https://q.uiver.app/#q=WzAsNSxbMSwzLCJcXGxhbmdsZSBcXHZiIG0gXFxyYW5nbGVfe1xcbWF0aGNhbCBNfSJdLFswLDIsIlxcbWF0aGNhbCBNIl0sWzIsMiwiXFxtYXRoY2FsIE4iXSxbMSwxLCJcXG1hdGhjYWwgQyJdLFsxLDAsIlxcbWF0aGNhbCBEIl0sWzAsMSwiIiwwLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoiaG9vayIsInNpZGUiOiJ0b3AifX19XSxbMiwzLCIiLDIseyJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJob29rIiwic2lkZSI6InRvcCJ9fX1dLFsxLDMsIiIsMCx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV0sWzAsMiwiZSIsMix7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV0sWzMsNCwiIiwwLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoiaG9vayIsInNpZGUiOiJ0b3AifX19XSxbMiw0LCJoIiwyLHsiY3VydmUiOjIsInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsxLDQsImciLDAseyJjdXJ2ZSI6LTIsInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==
\[\begin{tikzcd}
	& {\mathcal D} \\
	& {\mathcal C} \\
	{\mathcal M} && {\mathcal N} \\
	& {\langle \vb m \rangle_{\mathcal M}}
	\arrow[tail, from=4-2, to=3-1]
	\arrow[tail, from=3-3, to=2-2]
	\arrow[tail, from=3-1, to=2-2]
	\arrow["e"', tail, from=4-2, to=3-3]
	\arrow[tail, from=2-2, to=1-2]
	\arrow["h"', curve={height=12pt}, dashed, from=3-3, to=1-2]
	\arrow["g", curve={height=-12pt}, dashed, from=3-1, to=1-2]
\end{tikzcd}\]
    where \( \mathcal D \in \mathbb K \), and both \( \mathcal M, \mathcal N \) embed into \( \mathcal C \) and therefore into \( \mathcal D \).
    Note that \( g(\vb m) = h(\vb n) \).
    Replacing \( \mathcal D \) with an isomorphic copy if required, we may assume that \( h \) is an inclusion, so \( g(\vb m) = \vb n \).
    We know that \( (\mathcal M, \vb m) \) is a witnessing pair, so \( \mathcal M \vDash \varphi(\vb m) \).
    Then \( \mathcal D \vDash \varphi(g(\vb m)) \) as existential formulae are preserved under taking extensions.
    Since \( \mathcal N \) is existentially closed in \( \mathbb K \), \( \mathcal D \in \mathbb K \), and \( \mathcal N \subseteq \mathcal D \), we conclude that \( \mathcal N \vDash \varphi(g(\vb m)) \) so \( \mathcal N \vDash \varphi(\vb n) \) as required.
    % then use compactness twice to reduce to first order formula

    In particular, if \( \mathcal T \) is a theory axiomatising existentially closed structures in \( \mathbb K \), then \( \mathcal T \) has quantifier elimination by applying the completeness theorem and then using the syntactic criterion for quantifier elimination proven previously.
\end{proof}
\begin{example}
    We show that the theory \( \mathsf{ACF} \) of algebraically closed fields has quantifier elimination.
    First, recall that \( \mathsf{ACF} \) axiomatises the existentially closed fields, so it suffices to check that the class of substructures of fields has the amalgamation property.
    Note that a substructure of a field must satisfy all universal sentences in the theory of fields, so the substructures of fields are precisely the integral domains.
    General field theory shows that the class of fields has the amalgamation property; we can then prove that the class of integral domains has the amalgamation property by passing to fraction fields.
\end{example}
\begin{example}
    The theory \( \mathsf{DLO} \) of dense linear orders without endpoints has quantifier elimination.
    The class of substructures of dense linear orders has the amalgamation property: indeed, any two linear orders embed into a poset, which can be extended into a linear order by Zorn's lemma, and is thus a substructure of some dense linear order.
\end{example}

\subsection{Inductive classes}
\begin{definition}
    A class \( \mathbb K \) of \( \mathcal L \)-structures is \emph{inductive} if it is closed under isomorphisms and under unions of chains of embeddings.
\end{definition}
\begin{theorem}
    Let \( \mathcal M \) be a structure in an inductive class \( \mathbb K \).
    Then \( \mathcal M \subseteq \mathcal N \) for some \( \mathcal N \) existentially closed in \( \mathbb K \).
\end{theorem}
This is analogous to the theorem that every field has an algebraic closure, and is proven in a similar way.
\begin{proof}
    We show that \( \mathcal M \) can be extended to some structure \( \mathcal M^\star \in \mathbb K \) with the property that for all \( \vb m \in \mathcal M \) and \( \varphi(\vb x) \) an existential \( \mathcal L \)-formula, if \( \varphi(\vb m) \) holds in some extension of \( \mathcal M^\star \) in \( \mathbb K \), then \( \varphi(\vb m) \) holds in \( \mathcal M^\star \).

    We now show that this suffices to complete the proof.
    Indeed, we then recursively define a chain of \( \mathbb K \)-structures by setting \( \mathcal M^{(0)} = \mathcal M \) and \( \mathcal M^{(i+1)} = (\mathcal M^{(i)})^\star \), then taking their union to form \( \mathcal N \).
    Then \( \mathcal N \) lies in \( \mathbb K \) as \( \mathbb K \) is inductive, and moreover it extends \( \mathcal M \).

    This \( \mathcal N \) is existentially closed in \( \mathbb K \).
    Suppose \( \varphi(\vb x) \) is an existential formula, \( \vb n \in \mathcal N \), and \( \mathcal D \) is a structure in \( \mathbb K \) such that \( \mathcal D \vDash \varphi(\vb n) \).
    As \( \vb n \in \bigcup_{i < \omega} \mathcal M^{(i)} \) and the \( \mathcal M^{(i)} \) form a chain, there must be \( k < \omega \) such that \( \vb n \in \mathcal M^{(k)} \).
    Then \( (\mathcal M^{(k)})^\star = \mathcal M^{(k+1)} \vDash \varphi(\vb n) \), so in particular, \( \mathcal N \vDash \varphi(\vb n) \).

    We now construct \( \mathcal M^\star \).
    Using the axiom of choice, create an ordinal-indexed list of pairs \( (\varphi_\beta, \vb m_\beta)_\beta \) where \( \varphi \) is an existential formula and \( \vb m \in \mathcal M \), and \( \beta \) ranges over all ordinals less than some ordinal \( \delta \).
    We then construct a chain of \( \mathbb K \)-structures by transfinite induction.
    Let \( \mathcal M_0 = \mathcal M \).
    At each successor stage, let \( \mathcal M_{\beta + 1} \) be a \( \mathbb K \)-structure \( \mathcal D \) that extends \( \mathcal M_\beta \) and models \( \varphi_\beta(\vb m_\beta) \), if this exists.
    If such a model does not exist, define \( \mathcal M_{\beta + 1} = \mathcal M_\beta \).
    At each limit stage, let \( \mathcal M_\lambda = \bigcup_{\beta < \lambda} \mathcal M_\beta \).
    Finally, set \( \mathcal M^\star = \mathcal M_\delta \).

    If \( \varphi(\vb x) \) is existential, \( \vb m \in \mathcal M \), and \( \mathcal D \) is some \( \mathbb K \)-structure that extends \( \mathcal M^\star \) and models \( \varphi(\vb m) \), then \( (\varphi, \vb m) = (\varphi_\beta, \vb m_\beta) \) for some \( \beta < \delta \).
    Then \( \mathcal M_\beta \subseteq \mathcal M^\star \subseteq \mathcal D \), so \( \mathcal M_{\beta + 1} \) models \( \varphi_\beta(\vb m_\beta) = \varphi(\vb m) \) by definition.
    But as \( \varphi \) is existential and \( \mathcal M^\star \) extends \( \mathcal M_\beta \), we must also have that \( \mathcal M^\star \) models \( \varphi(\vb m) \), as required.
\end{proof}

\subsection{Characterisations of quantifier elimination}
\begin{theorem}
    Let \( \mathcal T \) be an \( \mathcal L \)-theory.
    Then the following are equivalent.
    \begin{enumerate}
        \item The theory \( \mathcal T \) is model-complete.
        \item Every model of \( \mathcal T \) is an existentially closed model of \( \mathcal T \).
        \item Given an embedding \( e : \mathcal A \rightarrowtail \mathcal B \) between models of \( \mathcal T \), there is an elementary extension \( \mathcal D \) of \( \mathcal A \) and an embedding \( g : \mathcal B \rightarrowtail D \) such that \( g \circ e = \id_{\mathcal A} \).
        \item For any quantifier-free \( \mathcal L \)-formula \( \varphi(\vb x, \vb y) \), the formula \( \exists \vb y.\, \varphi(\vb x, \vb y) \) is equivalent to some universal \( \mathcal L \)-formula \( \psi(\vb x) \) modulo \( \mathcal T \).
        \item Every \( \mathcal L \)-formula is equivalent to some universal \( \mathcal L \)-formula modulo \( \mathcal T \).
    \end{enumerate}
\end{theorem}
\begin{proof}
    \emph{(i) implies (ii).}
    As all embeddings between models are elementary, if a superstructure has a witness to an existential, so does the substructure.

    \emph{(ii) implies (iii).}
    We use the existential amalgamation theorem.
    Take \( S \) to be the set of all elements of \( \mathcal A \), then by (ii), \( (\mathcal B, e(S)) \to_1 (\mathcal A, S) \).
    We obtain
    % https://q.uiver.app/#q=WzAsNCxbMSwyLCJcXG1hdGhjYWwgQSJdLFswLDEsIlxcbWF0aGNhbCBBIl0sWzEsMCwiXFxtYXRoY2FsIEQiXSxbMiwxLCJcXG1hdGhjYWwgQiJdLFswLDEsIjFfQSJdLFsxLDIsIlxccHJlY2VxIl0sWzAsMywiZSIsMix7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1vbm8ifX19XSxbMywyLCJnIiwyLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibW9ubyJ9fX1dXQ==
\[\begin{tikzcd}
	& {\mathcal D} \\
	{\mathcal A} && {\mathcal B} \\
	& {\mathcal A}
	\arrow["{1_A}", from=3-2, to=2-1]
	\arrow["\preceq", from=2-1, to=1-2]
	\arrow["e"', tail, from=3-2, to=2-3]
	\arrow["g"', tail, from=2-3, to=1-2]
\end{tikzcd}\]
    as required.

    \emph{(iii) implies (iv).}
    It suffices to show that any universal formula \( \varphi(\vb x) \) is preserved under embeddings.
    If so, then \( \varphi(\vb x) \) is equivalent to an existential \( \mathcal L \)-formula, so in particular, any existential formula is equivalent to a universal formula.
    Let \( e : \mathcal A \rightarrowtail \mathcal B \) be an embedding.
    Then by (iii) we have an elementary extension \( \mathcal A \preceq \mathcal D \), so if \( \mathcal A \vDash \varphi(\vb a) \), then \( \mathcal D \vDash \varphi(\vb a) \), and as \( \mathcal B \) is a substructure of \( \mathcal D \), we have \( \mathcal B \vDash \varphi(e(\vb a)) \).
    The reverse implication follows from the fact that \( \varphi \) is universal.

    \emph{(iv) implies (v).}
    We proceed by induction on the structure of \( \mathcal L \)-formulae.
    We can iteratively convert existential quantifiers to universal quantifiers, noting that (iv) allows us to convert a sequence of existentials to a sequence of universals simultaneously.

    \emph{(v) implies (i).}
    We use induction on the structure of \( \mathcal L \)-formulae, noting that universal formulae are preserved under extensions, and that every formula and its negation can be represented as a universal formula.
\end{proof}
Let \( \mathcal M, \mathcal N \) be \( \mathcal L \)-structures.
If \( \mathcal M, \mathcal N \) satisfy the same quantifier-free sentences, we write \( \mathcal M \equiv_0 \mathcal N \).
\begin{theorem}
    Let \( \mathcal T \) be an \( \mathcal L \)-theory.
    Then the following are equivalent.
    \begin{enumerate}
        \item \( \mathcal T \) has quantifier elimination.
        \item If \( \mathcal A, \mathcal B \vDash \mathcal T \) and \( \vb a \in \mathcal A, \vb b \in \mathcal B \) are tuples of the same length, then \( (\mathcal A, \vb a) \equiv_0 (\mathcal B, \vb b) \) implies \( (\mathcal A, \vb a) \to_1 (\mathcal B, \vb b) \).
        \item Whenever \( \mathcal A, \mathcal B \vDash \mathcal T \), \( S \subseteq \mathcal A \) and \( e : \langle S \rangle_{\mathcal A} \rightarrowtail \mathcal B \), then there is an elementary extension \( \mathcal D \) of \( \mathcal B \) and an embedding \( f : \mathcal A \rightarrowtail \mathcal D \) extending \( e \).
        \item \( \mathcal T \) is model-complete and \( \mathcal T_\forall \) has the amalgamation property.
        \item For every quantifier-free \( \mathcal L \)-formula \( \varphi(\vb x, y) \), the formula \( \exists y.\, \varphi(\vb x, y) \) is \( \mathcal T \)-equivalent to a quantifier-free formula \( \psi(\vb x) \).
    \end{enumerate}
\end{theorem}
\begin{proof}
    (i) implies (ii) is clear.

    \emph{(ii) implies (iii).}
    It suffices to show that \( (\mathcal A, \vb a) \to_1 (\mathcal B, e(\vb a)) \) by the existential amalgamation theorem.
    Since a sentence in \( \mathcal L_S \) is finite, it can only mention finitely many of the new constants in \( S \), so it is enough to check that \( (\mathcal A, \vb a) \to_1 (\mathcal B, e(\vb a)) \) for all tuples \( \vb a \) obtainable from \( S \).
    Now, if \( \vb a \) is such a tuple and \( e : \langle S \rangle_{\mathcal A} \rightarrowtail \mathcal B \) is an embedding, then \( (\mathcal A, \vb a) \equiv_0 (\mathcal B, e(\vb a)) \), giving the required result by (ii).

    \emph{(iii) implies (iv).}
    By the previous theorem, to check model-completeness it suffices to check that for each embedding \( h : \mathcal M \rightarrowtail \mathcal N \) between models of \( \mathcal T \), there is an elementary extension \( \mathcal D \) of \( \mathcal M \) and an embedding \( g : \mathcal N \to \mathcal D \) such that \( g \circ h = \id_{\mathcal M} \).
    Consider the instance of (iii) where \( S = h(\mathcal M) \) and \( e = h^{-1} \) as a map \( h(\mathcal M) \similarrightarrow \mathcal M \).
    Then there is an elementary extension \( \mathcal D \) of \( \mathcal M \) and an embedding \( g : \mathcal M \rightarrowtail \mathcal D \) extending \( e \).
    % https://q.uiver.app/#q=WzAsNCxbMSwyLCJcXGxhbmdsZSBTIFxccmFuZ2xlX3tcXG1hdGhjYWwgTn0gPSBoKFxcbWF0aGNhbCBNKSJdLFswLDEsIlxcbWF0aGNhbCBOIl0sWzEsMCwiXFxtYXRoY2FsIEQiXSxbMiwxLCJcXG1hdGhjYWwgTSJdLFswLDEsIiIsMCx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV0sWzEsMiwiZyIsMCx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV0sWzAsMywiZSIsMl0sWzMsMiwiXFxwcmVjZXEiLDIseyJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJob29rIiwic2lkZSI6InRvcCJ9fX1dXQ==
\[\begin{tikzcd}
	& {\mathcal D} \\
	{\mathcal N} && {\mathcal M} \\
	& {\langle S \rangle_{\mathcal N} = h(\mathcal M)}
	\arrow[tail, from=3-2, to=2-1]
	\arrow["g", tail, from=2-1, to=1-2]
	\arrow["e"', from=3-2, to=2-3]
	\arrow["\preceq"', tail, from=2-3, to=1-2]
\end{tikzcd}\]
    This means that for all \( m \in \mathcal M \), we have \( g(h(m)) = e(h(m)) = m \).
    To see that \( \mathcal T_\forall \) has the amalgamation property, consider models \( \mathcal A', \mathcal B', \mathcal C \) of \( \mathcal T_\forall \) where \( \mathcal C \) embeds into both \( \mathcal A' \) and \( \mathcal B' \).
    Models of \( \mathcal T_\forall \) are precisely the substructures of models of \( \mathcal T \), so \( \mathcal A' \) and \( \mathcal B' \) are substructures of models \( \mathcal A \) and \( \mathcal B \) of \( \mathcal T \) respectively.
    Consider the instance of (iii) where \( S = \mathcal C = \langle \mathcal C \rangle_{\mathcal A} \) and \( e \) is the embedding of \( \mathcal C \) into \( \mathcal B \).
    Then we have an elementary extension \( \mathcal D \) of \( \mathcal B \) and an embedding \( f : A \rightarrowtail \mathcal D \) that extends \( e \).
    % https://q.uiver.app/#q=WzAsNixbMSwzLCJcXG1hdGhjYWwgQyJdLFsyLDIsIlxcbWF0aGNhbCBCJyJdLFswLDIsIlxcbWF0aGNhbCBBJyJdLFsyLDEsIlxcbWF0aGNhbCBCIl0sWzAsMSwiXFxtYXRoY2FsIEEiXSxbMSwwLCJcXG1hdGhjYWwgRCJdLFswLDEsIiIsMCx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV0sWzAsMiwiIiwyLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoiaG9vayIsInNpZGUiOiJ0b3AifX19XSxbMSwzLCIiLDAseyJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJob29rIiwic2lkZSI6InRvcCJ9fX1dLFsyLDQsIiIsMix7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV0sWzMsNSwiXFxwcmVjZXEiLDJdLFs0LDUsImYiLDAseyJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJob29rIiwic2lkZSI6InRvcCJ9fX1dXQ==
\[\begin{tikzcd}
	& {\mathcal D} \\
	{\mathcal A} && {\mathcal B} \\
	{\mathcal A'} && {\mathcal B'} \\
	& {\mathcal C}
	\arrow[tail, from=4-2, to=3-3]
	\arrow[tail, from=4-2, to=3-1]
	\arrow[tail, from=3-3, to=2-3]
	\arrow[tail, from=3-1, to=2-1]
	\arrow["\preceq"', from=2-3, to=1-2]
	\arrow["f", tail, from=2-1, to=1-2]
\end{tikzcd}\]
    Now, \( \mathcal D \equiv \mathcal B \vDash \mathcal T \vdash \mathcal T_\forall \), we must have that \( \mathcal D \) is a model of \( \mathcal T_\forall \) giving the amalgamation property as desired.

    \emph{(iv) implies (v).}
    Model-completeness implies that every model of \( \mathcal T \) is an existentially closed model of \( \mathcal T \).
    Then, by the theorem characterising theories axiomatising existentially closed structures, this proof is complete, as the models of \( \mathcal T_\forall \) are precisely the substructures of models of \( \mathcal T \).

    \emph{(v) implies (i).}
    Immediate from the syntactic criterion for quantifier elimination.
\end{proof}
\begin{corollary}
    Let \( \mathcal A \) be a finite \( \mathcal L \)-structure.
    The theory \( \mathrm{Th}(\mathcal A) \) of \( \mathcal A \) has quantifier elimination if and only if every isomorphism between finitely generated substructures of \( \mathcal A \) can be extended to an automorphism of \( \mathcal A \).
\end{corollary}
% The property that every isomorphism between finitely generated substructures of \( \mathcal A \) can be extended to an automorphism of \( \mathcal A \) appears in various places throughout model theory.
\begin{proof}
    For the forward direction, consider case (iii) of the previous theorem applied to \( \mathcal A = \mathcal B \) where \( e \) is the composite \( \langle \vb a \rangle_{\mathcal A} \similarrightarrow \langle \vb b \rangle_{\mathcal A} \rightarrowtail \mathcal A \).
    We obtain an elementary extension \( \mathcal D \) of \( \mathcal A \).
    If \( \abs{\mathcal A} = n < \aleph_0 \), then the theory of \( \mathcal A \) must include a sentence that states this fact.
    Thus \( \mathcal D \) models the same sentence, so \( \abs{\mathcal D} = n = \abs{\mathcal A} \).
    Thus \( \mathcal A \) and \( \mathcal D \) are elementarily equivalent finite structures, so the elementary embedding \( h : \mathcal A \rightarrowtail \mathcal D \) is an isomorphism.
    % https://q.uiver.app/#q=WzAsNSxbMCwxLCJcXGxhbmdsZSBcXHZiIGEgXFxyYW5nbGVfe1xcbWF0aGNhbCBBfSJdLFsyLDEsIlxcbGFuZ2xlIFxcdmIgYiBcXHJhbmdsZV97XFxtYXRoY2FsIEF9Il0sWzIsMCwiXFxtYXRoY2FsIEEiXSxbMSwwLCJcXG1hdGhjYWwgRCJdLFswLDAsIlxcbWF0aGNhbCBBIl0sWzAsMSwiXFxzaW0iXSxbMSwyLCIiLDAseyJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJob29rIiwic2lkZSI6InRvcCJ9fX1dLFszLDIsImheey0xfSJdLFswLDQsIiIsMix7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV0sWzQsMywiZiIsMCx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV1d
\[\begin{tikzcd}
	{\mathcal A} & {\mathcal D} & {\mathcal A} \\
	{\langle \vb a \rangle_{\mathcal A}} && {\langle \vb b \rangle_{\mathcal A}}
	\arrow["\sim", from=2-1, to=2-3]
	\arrow[tail, from=2-3, to=1-3]
	\arrow["{h^{-1}}", from=1-2, to=1-3]
	\arrow[tail, from=2-1, to=1-1]
	\arrow["f", tail, from=1-1, to=1-2]
\end{tikzcd}\]
    Now, as \( \abs{\mathcal A} = \abs{\mathcal D} = n < \aleph_0 \) and \( f \) is an embedding, it must also be surjective by the pigeonhole principle, and thus an isomorphism.
    Hence \( h^{-1} \circ f \) is an automorphism of \( \mathcal A \) extending our isomorphism \( \langle \vb a \rangle_{\mathcal A} \similarrightarrow \langle \vb b \rangle_{\mathcal A} \), as required.

    For the converse, we prove case (ii) in the previous theorem.
    Let \( \vb b \in \mathcal B \vDash \mathrm{Th}(\mathcal A) \) and \( \vb c \in \mathcal C \vDash \mathrm{Th}(\mathcal A) \) be tuples of the same length.
    As \( \mathrm{Th}(\mathcal A) \) is a complete theory, the models \( \mathcal B \) and \( \mathcal C \) are elementarily equivalent to \( \mathcal A \), and thus by finiteness they are isomorphic.
    Thus, without loss of generality, we can set \( \mathcal A = \mathcal B = \mathcal C \).
    By hypothesis, \( (\mathcal A, \vb b) \equiv_0 (\mathcal A, \vb c) \).
    Thus we obtain an isomorphism \( \langle \vb b \rangle_{\mathcal A} \similarrightarrow \langle \vb c \rangle_{\mathcal A} \) mapping \( \vb b \) to \( \vb c \), which can be extended to an automorphism of \( \mathcal A \) by assumption.
    If \( \vb m \) is a witness to
    \[ (\mathcal A, \vb b) \vDash \exists \vb y.\, \varphi(\vb b, \vb y) \]
    then \( f(\vb m) \) must witness the truth of
    \[ (\mathcal A, \vb c) \vDash \exists \vb y.\, \varphi(\vb c, \vb y) \]
    Thus, \( (\mathcal A, \vb b) \to_1 (\mathcal A, \vb c) \) as required.
\end{proof}
\begin{example}
    Let \( V \) be a finite vector space.
    Any isomorphism between subspaces can be extended to an automorphism using the Steinitz exchange lemma, so \( \mathrm{Th}(V) \) has quantifier elimination.
\end{example}
\begin{corollary}
    Let \( \mathcal T \) be an \( \mathcal L \)-theory such that
    \begin{enumerate}
        \item If \( \mathcal A, \mathcal B \vDash \mathcal T \) with \( \mathcal A \subseteq \mathcal B \), and \( \varphi(\vb x, y) \) is a quantifier-free formula, then for all \( \vb a \in \mathcal A \),
        \[ (\mathcal B \vDash \exists y.\, \varphi(\vb a, y)) \implies (\mathcal A \vDash \exists y.\, \varphi(\vb a, y)) \]
        \item For any \( \mathcal C \subseteq \mathcal A \vDash \mathcal T \), there is an \emph{initial intermediate model} \( \mathcal A' \vDash \mathcal T \): that is, \( \mathcal C \subseteq \mathcal A' \subseteq \mathcal A \), and for any other model \( \mathcal C \subseteq \mathcal B \subseteq \mathcal A \), there is an embedding \( \mathcal A' \rightarrowtail \mathcal B \) that fixes \( \mathcal C \).
    \end{enumerate}
    Then \( \mathcal T \) has quantifier elimination.
\end{corollary}
\begin{proof}
    We show that condition (ii) of the theorem above holds.
    Let \( \mathcal A, \mathcal B \) be models of \( \mathcal T \), and \( \vb a \in \mathcal A, \vb b \in \mathcal B \) be such that \( (\mathcal A, \vb a) \equiv_0 (\mathcal B, \vb b) \).
    It suffices to show that \( (\mathcal A, \vb a) \to_1 (\mathcal B, \vb b) \).
    Let \( \varphi(\vb x, y) \) be quantifier-free, and such that \( \mathcal A \vDash \exists \vb y.\, \varphi(\vb a, \vb y) \).
    Let \( \vb c = (c_0, \dots, c_{k-1}) \in \mathcal A \) be such a witness, so \( \mathcal A \vDash \varphi(\vb a, \vb c) \).

    We claim that there is an elementary extension \( \mathcal B_0 \) of \( \mathcal B \) and an element \( d_0 \in \mathcal B_0 \) such that \( (\mathcal A, \vb a, c_0) \equiv_0 (\mathcal B_0, \vb b, d_0) \).
    If we can do this, we can iterate the process to obtain a chain of elementary extensions
    \[ \mathcal B \preceq \mathcal B_0 \preceq \mathcal B_1 \preceq \dots \preceq \mathcal B_{k-1} \]
    and elements \( d_i \in \mathcal B_i \) such that \( (\mathcal A, \vb a, \vb c) \equiv_0 (\mathcal B, \vb b, \vb d) \).
    Then \( \mathcal B_{k-1} \vDash \varphi(\vb b, \vb d) \) as \( \varphi \) is quantifier-free, so \( \mathcal B_{k-1} \vDash \exists y.\, \varphi(\vb b, \vb y) \), giving \( \mathcal B \vDash \exists y.\, \varphi(\vb b, \vb y) \) as \( \mathcal B_{k-1} \equiv \mathcal B \) as required.

    To find \( \mathcal B_0 \) and \( d_0 \), we use the hypotheses and the compactness theorem.
    As \( (\mathcal A, \vb a) \equiv_0 (\mathcal B, \vb b) \), there is an isomorphism \( \langle \vb a \rangle_{\mathcal A} \to \langle \vb b \rangle_{\mathcal B} \).
    Take \( \mathcal C = \langle \vb a \rangle_{\mathcal A} \subseteq \mathcal A \).
    By hypothesis (ii), there is an initial intermediate model \( \mathcal C \subseteq \mathcal A' \subseteq \mathcal A \) with \( \mathcal A' \vDash \mathcal T \), and there is an embedding \( \mathcal A' \rightarrowtail \mathcal B \) fixing \( \mathcal C \).
    Without loss of generality, let us assume that this embedding is an inclusion.
    Write
    \[ \Psi = \qty{\psi(\vb x, y) \mid \mathcal A \vDash \psi(\vb a, c_0),\, \psi \text{ quantifier-free}} \]
    As \( \vb a \in \mathcal A' \), we have that \( \mathcal A' \vDash \exists y.\, \psi(\vb a, y) \) for all \( \psi \in \Psi \) by hypothesis (a).
    Now, \( \mathcal A' \subseteq \mathcal B \), and existential formulae are preserved under extension, so \( \mathcal B \vDash \exists y.\, \psi(\vb b, y) \) for all \( \psi \in \Psi \).
    We conclude that every finite subset of \( \Psi \) is satisfied by some element of \( \mathcal B \), as finite conjunctions of quantifier-free formulae are also quantifier-free.
    Thus, by compactness, there is an elementary extension \( \mathcal B \preceq \mathcal B_0 \) and \( d_0 \in \mathcal B_0 \) satisfying the formulae in \( \Psi \).
    In particular, \( (\mathcal A, \vb a, c_0) \equiv_0 (\mathcal B_0, \vb b, d_0) \).
\end{proof}

\subsection{Applications}
\begin{example}
    The theory \( \mathsf{RCF} \) of \emph{real closed fields} is the theory of ordered fields for which every nonnegative element is a square, and that all odd polynomials have a root.
    Equivalently, it is the theory of ordered fields elementarily equivalent to \( \mathbb R \).
    We show that this theory, with signature \( (+, \times, 0, 1, <) \), has quantifier elimination.
    We will assume that every ordered field has a \emph{real closure}, and that a real closed field satisfies the intermediate value theorem for polynomials.

    We show that hypothesis (i) of the corollary above holds.
    Suppose we have an embedding \( \mathcal A \subseteq \mathcal B \) of real closed fields, \( \vb a \in A \), and a quantifier-free formula \( \varphi(\vb x, y) \) such that \( \mathcal B \vDash \exists y.\, \varphi(\vb a, y) \).
    By considering the disjunctive normal form, we may assume that \( \varphi \) is a disjunction of a conjunction of literals.
    Moreover, the formulae \( y \neq z \) and \( y \nless z \) can be written in terms of \( = \) and \( < \).
    Thus, we may assume that \( \varphi(\vb a, y) \) is of the form
    \[ \qty(\bigwedge_{i < r} p_i(y) = 0) \vee \qty(\bigwedge_{j < s} 0 < q_j(y)) \]
    where \( p_i, q_j \) are polynomials with coefficients in \( \mathcal A \).
    If \( \varphi \) contains a nontrivial equation \( p_i(y) = 0 \), then if a witness exists in \( \mathcal B \), it must be algebraic over \( \mathcal A \).
    One can show algebraically that this witness must lie in \( \mathcal A \).
    Therefore, let us suppose \( r = 0 \).

    There are only finitely many points \( c_0, \dots, c_{n-1} \in \mathcal A \) that are roots for the \( q_j(y) \).
    Since the real closed fields satisfy the intermediate value theorem for polynomials, the \( q_j(y) \) can only change sign at the \( c_i \).
    Note that
    \[ \mathcal A \vDash \forall x y.\, x < y \to \exists z.\, (x < z \wedge z < y) \]
    Since the \( c_i \) lie in \( \mathcal A \), there is an element of \( \mathcal A \) between any pair of distinct \( c_i \).
    Suppose \( b \) witnesses \( \exists y.\, \varphi(\vb a, y) \) in \( \mathcal B \).
    If there is a smallest interval \( (c_i, c_j) \) containing \( \mathcal B \), we can pick \( a \in \mathcal A \) also inside this interval, giving \( \mathcal A \vDash \varphi(\vb a, a) \) as required.
    The other cases are similar.

    We now show hypothesis (ii).
    Suppose \( \mathcal C \subseteq \mathcal A \) where \( \mathcal A \) is a real closed field.
    Then \( \mathcal C \) is an ordered integral domain.
    The field of fractions of \( \mathcal C \) can be made an ordered field in a canonical way, by saying \( \frac{a}{b} > 0 \) if \( ab > 0 \).
    The embedding \( \mathcal C \) into \( \mathcal A \) is an injective homomorphism of ordered rings, into an ordered field.
    By the universal property of the fraction field, there is a unique homomorphism of ordered fields from \( FF(\mathcal C) \) to \( \mathcal A \) that extends the inclusion of \( \mathcal C \) into \( \mathcal A \).
    Let \( \mathcal A' \) be the real closure of \( FF(\mathcal C) \), so that \( \mathcal C \subseteq FF(\mathcal C) \subseteq \mathcal A' \subseteq \mathcal A \).
    If \( \mathcal B \vDash \mathsf{RCF} \) and \( \mathcal C \subseteq B \), then by the same argument we have a unique ordered ring homomorphism \( FF(\mathcal C) \to \mathcal B \) extending the embedding \( \mathcal C \subseteq \mathcal B \).
    Thus \( \mathcal A' \subseteq \mathcal B \) as well, and this embedding fixes \( \mathcal C \).
\end{example}
\begin{corollary}[Hilbert's Nullstellensatz]
    Let \( k \) be an algebraically closed field, and \( I \) be a proper ideal of \( k[x_1, \dots, x_n] \).
    Then there exists \( \vb a \in k^n \) such that \( f(\vb a) = 0 \) for all \( I \in f \).
\end{corollary}
\begin{proof}
    By Zorn's lemma, every proper ideal can be extended to a maximal ideal, so without loss of generality we may assume that \( I \) is a maximal ideal.
    Let \( L \) be the residue field \( \faktor{k[x_1, \dots, x_n]}{I} \), and let \( \overline L \) be its algebraic closure.
    By Hilbert's basis theorem, there exists a finite set of generators \( f_1, \dots, f_r \) for \( I \).
    Note that \( \vb 0 \) is a witness to
    \[ \overline L \vDash \exists \vb x.\, \qty(f_1(\vb x) = 0 \wedge \dots \wedge f_r(\vb x) = 0) \]
    We have embeddings \( k \subseteq L \subseteq \overline L \), where both \( k \) and \( \overline L \) are algebraically closed fields.
    The theory of algebraically closed fields has quantifier elimination, so is model-complete.
    Thus the embedding \( k \subseteq \overline L \) is elementary, so
    \[ k \vDash \exists \vb x.\, \qty(f_1(\vb x) = 0 \wedge \dots \wedge f_r(\vb x) = 0) \]
    We can then take \( \vb a \) to be a witness to this existential.
\end{proof}
\begin{corollary}[Chevalley's theorem]
    Let \( k \) be an algebraically closed field.
    Then the image of a constructible set in \( k^n \) under a polynomial map is constructible.
\end{corollary}
\begin{proof}
    The quantifier-free-definable subsets of \( k^n \) are precisely the finite Boolean combinations of the Zariski closed subsets of \( k^n \), which are by definition the constructible sets.
    As \( \mathsf{ACF} \) has quantifier elimination, these are exactly the definable subsets using arbitrary formulae.
    Now, if \( X \subseteq k^n \) is constructible and \( p : k^n \to k^m \) is a polynomial map, then
    \[ p(X) = \qty{y \in k^m \mid \exists x.\, p(x) = y} \]
    This is definable in the same language, so is a constructible set.
\end{proof}
